Reffect{-}discrete($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case Reffect{-}f($A$) of inl($f$) =$>$ tt $\mid$ inr($f$) =$>$ ff